\begin{tabbing}
$\forall$$L$:Knd List, $l$:IdLnk, ${\it tg}$:Id.
\\[0ex]@source($l$): only $L$ sends on ($l$ with ${\it tg}$) $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@source($l$): only $L$ sends on ($l$ with ${\it tg}$) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]$\forall$$e$:E.
\\[0ex]loc($e$) $=$ destination($l$) $\in$ Id $\Rightarrow$ kind($e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ (kind(sender($e$)) $\in$ $L$))
\-\-
\end{tabbing}